MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq() -> eq() , eq() -> true() , eq() -> false() , inf(X) -> cons() , take(0(), X) -> nil() , take(s(), cons()) -> cons() , length(cons()) -> s() , length(nil()) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { eq() -> true() , eq() -> false() , inf(X) -> cons() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [eq] = [3] [true] = [1] [false] = [1] [inf](x1) = [3] x1 + [3] [cons] = [0] [take](x1, x2) = [2] x1 + [3] x2 + [0] [0] = [0] [nil] = [0] [s] = [0] [length](x1) = [2] x1 + [0] This order satisfies the following ordering constraints: [eq()] = [3] >= [3] = [eq()] [eq()] = [3] > [1] = [true()] [eq()] = [3] > [1] = [false()] [inf(X)] = [3] X + [3] > [0] = [cons()] [take(0(), X)] = [3] X + [0] >= [0] = [nil()] [take(s(), cons())] = [0] >= [0] = [cons()] [length(cons())] = [0] >= [0] = [s()] [length(nil())] = [0] >= [0] = [0()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq() -> eq() , take(0(), X) -> nil() , take(s(), cons()) -> cons() , length(cons()) -> s() , length(nil()) -> 0() } Weak Trs: { eq() -> true() , eq() -> false() , inf(X) -> cons() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { take(0(), X) -> nil() , length(cons()) -> s() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [eq] = [3] [true] = [1] [false] = [1] [inf](x1) = [3] x1 + [3] [cons] = [0] [take](x1, x2) = [1] x1 + [3] x2 + [0] [0] = [1] [nil] = [0] [s] = [0] [length](x1) = [2] x1 + [1] This order satisfies the following ordering constraints: [eq()] = [3] >= [3] = [eq()] [eq()] = [3] > [1] = [true()] [eq()] = [3] > [1] = [false()] [inf(X)] = [3] X + [3] > [0] = [cons()] [take(0(), X)] = [3] X + [1] > [0] = [nil()] [take(s(), cons())] = [0] >= [0] = [cons()] [length(cons())] = [1] > [0] = [s()] [length(nil())] = [1] >= [1] = [0()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq() -> eq() , take(s(), cons()) -> cons() , length(nil()) -> 0() } Weak Trs: { eq() -> true() , eq() -> false() , inf(X) -> cons() , take(0(), X) -> nil() , length(cons()) -> s() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { length(nil()) -> 0() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [eq] = [3] [true] = [1] [false] = [1] [inf](x1) = [3] x1 + [3] [cons] = [0] [take](x1, x2) = [2] x1 + [3] x2 + [0] [0] = [0] [nil] = [0] [s] = [0] [length](x1) = [2] x1 + [1] This order satisfies the following ordering constraints: [eq()] = [3] >= [3] = [eq()] [eq()] = [3] > [1] = [true()] [eq()] = [3] > [1] = [false()] [inf(X)] = [3] X + [3] > [0] = [cons()] [take(0(), X)] = [3] X + [0] >= [0] = [nil()] [take(s(), cons())] = [0] >= [0] = [cons()] [length(cons())] = [1] > [0] = [s()] [length(nil())] = [1] > [0] = [0()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq() -> eq() , take(s(), cons()) -> cons() } Weak Trs: { eq() -> true() , eq() -> false() , inf(X) -> cons() , take(0(), X) -> nil() , length(cons()) -> s() , length(nil()) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { take(s(), cons()) -> cons() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [eq] = [3] [true] = [2] [false] = [3] [inf](x1) = [3] x1 + [3] [cons] = [0] [take](x1, x2) = [1] x1 + [3] x2 + [0] [0] = [0] [nil] = [0] [s] = [1] [length](x1) = [2] x1 + [1] This order satisfies the following ordering constraints: [eq()] = [3] >= [3] = [eq()] [eq()] = [3] > [2] = [true()] [eq()] = [3] >= [3] = [false()] [inf(X)] = [3] X + [3] > [0] = [cons()] [take(0(), X)] = [3] X + [0] >= [0] = [nil()] [take(s(), cons())] = [1] > [0] = [cons()] [length(cons())] = [1] >= [1] = [s()] [length(nil())] = [1] > [0] = [0()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq() -> eq() } Weak Trs: { eq() -> true() , eq() -> false() , inf(X) -> cons() , take(0(), X) -> nil() , take(s(), cons()) -> cons() , length(cons()) -> s() , length(nil()) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..